|
Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. One way of classifying formulas is by the amount of quantification. Formulae with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulae as the simplest. A theory has quantifier elimination if for every formula , there exists another formula without quantifiers that is equivalent to it (modulo the theory). == Examples == Examples of theories that have been shown decidable using quantifier elimination are Presburger arithmetic,〔 algebraically closed fields, real closed fields,〔 atomless Boolean algebras, term algebras, dense linear orders,〔 random graphs, Feature trees, as well as many of their combinations such as Boolean Algebra with Presburger arithmetic, and Term Algebras with Queues. Quantifier eliminator for the theory of the real numbers as an ordered additive group is ''Fourier–Motzkin elimination''; for the theory of the field of real numbers it is the ''Tarski–Seidenberg theorem''. Quantifier elimination can also be used to show that "combining" decidable theories leads to new decidable theories. Such constructions include the Feferman-Vaught theorem and Term Powers. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「quantifier elimination」の詳細全文を読む スポンサード リンク
|